benchmark respectTransparency#236
Draft
datokrat wants to merge 141 commits into
Draft
Conversation
Lean PR leanprover/lean4#13637 splits `@[implicit_reducible]` into `@[instance_reducible]` (TC tier) and `@[implicit_reducible]` (implicit-arg defeq tier). `instance` auto-stamps `.instanceReducible`, but `to_additive` calls `addInstance` directly for the additive copy, so the auto-stamp doesn't fire on the target. Extend `copyInstanceAttribute` to copy `.instanceReducible` in addition to the pre-existing `.implicitReducible`. Fixes the cascade in `Mathlib/Algebra/CharZero/Defs.lean`, `Ring/Defs.lean`, `AddTorsor/Defs.lean`, `Homology/HasNoLoop.lean`, `Matrix/DMatrix.lean`, `Group/Basic.lean`, `Group/WithOne/Defs.lean`, and `Order/Lattice.lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lean PR leanprover/lean4#13637 splits the unified `@[implicit_reducible]` into two tiers: * `@[instance_reducible]` — unfolds during type class search (the new `.instances` tier), used for declarations that participate in instance forwarding chains. * `@[implicit_reducible]` — unfolds only during implicit value-argument defeq (the new `.implicit` tier), used for narrower cases like functor laws. Most Mathlib uses of `@[implicit_reducible]` were on "reducible non-instance" helpers (`Function.Injective.distribLattice`, `SemilatticeSup.mk'`, `Lattice.mk'`, all of `Order/Copy.lean`, `Denumerable.mk'`, `Set.monoid`, `CreatesLimitOf*`, etc.) that build typeclass instances. Under the new semantics these must be tagged `@[instance_reducible]` for type class search to unfold them. This commit replaces all 818 `@[implicit_reducible]` annotations (including the 110 inline `(attr := implicit_reducible ...)` forms inside `@[to_additive]` / `@[to_dual]`) with `@[instance_reducible]` across the library. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Archive and tests Complements the main migration in Mathlib/ by covering the remaining sites in Archive/ and MathlibTest/. * Archive/Imo/Imo2019Q2.lean * Archive/MinimalSheffer.lean * MathlibTest/DefEqAbuse.lean * MathlibTest/InferInstanceAsPercent.lean (also updates the docstring expectations to reflect the new attribute name that `instance` now auto-stamps) * MathlibTest/fast_instance.lean (same docstring update) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…le]` tier split Adapted from Sébastien Gouëzel's MWE on Zulip [1]. Pins three claims about the tier split introduced in lean#13637: 1. Without any extra attribute, TC search distinguishes the two `SGMonoidal` instances at `F ⋙ (G ⋙ H)` and `(F ⋙ G) ⋙ H`, so an `rfl` between their `n` fields rightfully fails. 2. Tagging `Functor.comp` `[implicit_reducible]` (the narrower value-defeq-only tier) does NOT corrupt the above — the `[implicit_reducible]` corruption Sébastien warned about is gone. 3. Tagging `Functor.comp` `[instance_reducible]` (the TC tier) deliberately reproduces the pre-split corruption: `rfl` succeeds even though the two instances are mathematically distinct. This pins the upper-bound semantics — if a future change accidentally narrowed `[instance_reducible]`, this case would notice. [1]: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/592439262 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This reverts commit f9fa065.
Author
|
!bench |
|
Benchmark results for ae4dd50 against 8a9ccb2 are in. There are significant results. @datokrat
Large changes (3✅, 2🟥)
Medium changes (12✅, 8🟥)
Small changes (41✅, 209🟥) Too many entries to display here. View the full report on radar instead. |
Author
|
!bench |
|
Benchmark results for bc185d9 against 8a9ccb2 are in. There are significant results. @datokrat
No significant changes detected. |
Author
|
!bench |
|
Benchmark results for bc185d9 against 8a9ccb2 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @datokrat
No significant changes detected. |
Author
|
!bench |
|
Benchmark results for 737aa15 against 8a9ccb2 are in. There are significant results. @datokrat
Large changes (3✅)
Medium changes (11✅, 5🟥)
Small changes (40✅, 159🟥) Too many entries to display here. View the full report on radar instead. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.